2024-10-25 Functional Programming in Lean
Adding a Reader to Any Monad
code:lean
-- # Init.Prelude
/--
An implementation of Haskell's [ReaderT]. This is a monad transformer which
equips a monad with additional read-only state, of type ρ.
-/
def ReaderT (ρ : Type u) (m : Type u → Type v) (α : Type u) : Type (max u v) :=
ρ → m α
code:lean
-- # Init.Prelude
/-- Similar to MonadReaderOf, but ρ is an outParam for convenience. -/
class MonadReader (ρ : outParam (Type u)) (m : Type u → Type v) where
/-- (← read) : ρ reads the state out of monad m. -/
read : m ρ
確率のモナド
型強制(coercion)
code:lean
/--
A function for lifting a computation from an inner Monad to an outer Monad.
Like Haskell's [MonadTrans], but n does not have to be a monad transformer.
Alternatively, an implementation of [MonadLayer] without layerInvmap (so far).
-/
class MonadLift (m : semiOutParam (Type u → Type v)) (n : Type u → Type w) where
/-- Lifts a value from monad m into monad n. -/
monadLift : {α : Type u} → m α → n α